Skip to content

Store diagnostic hints as a list - #410

Merged
CatarinaGamboa merged 1 commit into
mainfrom
feat/hint-list
Oct 23, 2026
Merged

CatarinaGamboa merged 1 commit into
mainfrom
feat/hint-list

Conversation

@CatarinaGamboa

Copy link
Copy Markdown
Collaborator

First PR of a stack that adds state hints: when a typestate call fails, the error says which calls would make it verify.

Description

LJDiagnostic stored a single hint string. It now stores a list of Hint(kind, message) so a diagnostic can carry several hints and clients can show or filter them by kind:

  • addHint(Hint) replaces setHint(String); getHints() returns the list.
  • getHint() still returns the messages joined one per line (or null), so the terminal output and the vscode server (LJDiagnosticDTO uses getHint()) are unchanged.
  • Hint.Kind only has GENERAL for now; the next PRs add the kinds they use.
  • ExternalMethodNotFoundWarning adds its overloads hint in the constructor instead of overriding getHint().

No behavior change.

Type of change

  • Code refactoring

Checklist

  • Added tests: LJDiagnosticTest (no hints, order and joining)
  • mvn test passes locally

🤖 Generated with Claude Code

A diagnostic can now carry several hints, each with a kind, so clients
can show or filter them separately. getHint() still returns their
messages joined one per line, so existing clients keep working.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
@CatarinaGamboa
CatarinaGamboa added this pull request to stack #415 October 23, 2026 16:59
@CatarinaGamboa
CatarinaGamboa merged commit 2553ecd into main Oct 23, 2026
1 check passed
@CatarinaGamboa
CatarinaGamboa deleted the feat/hint-list branch October 23, 2026 17:43
@CatarinaGamboa
CatarinaGamboa restored the feat/hint-list branch October 23, 2026 17:44
CatarinaGamboa added a commit to liquid-java/vscode-liquidjava that referenced this pull request Oct 25, 2026
## Why
Until now, the state machine view got the receiver's possible and
accepted states from liquidjava-fsm, which re-read the error's
`expected` and `found` predicates as text. The verifier now computes
those states with the SMT solver and reports them on
`StateRefinementError#getContext()` (liquid-java/liquidjava#421). fsm
0.2.0 dropped its error context and only draws diagrams
(liquid-java/liquidjava-fsm#12). This PR switches the view to the
verifier's answer, so the diagram never contradicts the error next to
it.

## What
**Dependencies:** liquidjava-verifier 0.0.36, liquidjava-fsm 0.2.0 and
Spoon 11.5.0, the version the verifier now uses.

**Server**
- `StateRefinementErrorDTO` builds the diagram with
`StateMachineParser.parse(declaration file, context.receiverClass())`,
so a file that declares several classes shows the receiver's class.
- The new `StateMachineDTO` and `StateErrorContextDTO` keep the shape
the webview already reads (`stateMachine.errorContext`). The error
context now has `calledMethod`, `receiver`, `possibleStates`,
`acceptedStates`, `validStates` and `invalidStates`.
- The verifier names each state in every state set. The diagram shows
the first set, and a state is marked so that the marks are never wrong:
- It is **valid** only if the call is accepted in *every* possible
combination with that state.
  - It is **invalid** only if the call is accepted in *none* of them.
- Otherwise it stays unmarked. When the accepted states depend on the
arguments, nothing is marked.
  - With one state set, this gives the same marks as before.

**Client**
- `getStateErrorFocus` uses the server's lists directly. The fallbacks
to `definiteFoundState` and `actualStates` are gone, and so are
`expectedCondition` and `foundCondition`, which nothing displayed.

**Fixed:** the `setHint` test, which broke when hints became a list
(liquid-java/liquidjava#410).

Output for the fsm study fixtures (DatagramSocket and tree node),
serialized by the server:
```json
{"calledMethod":"receive","receiver":"socket","possibleStates":["bound","closed"],"acceptedStates":["unbound","bound","connected"],"validStates":["bound"],"invalidStates":["closed"]}
{"calledMethod":"getFirstChild","receiver":"root","possibleStates":["childrenAllowed"],"acceptedStates":["maybeHasChildren"],"validStates":[],"invalidStates":["childrenAllowed"]}
```
These are the same marks the view showed before for these examples.

## Follow-ups
- One diagram per `@StateSet` (#115, #116,
liquid-java/liquidjava-fsm#8), e.g. ImageWriteParam.
- Send the hints as a list (with their kind) and the error category.
- Cache the diagram per class instead of parsing the file for each
error.

## Tests
- Server: `mvn test`, 27 tests pass, including the new
`StateErrorContextDTOTest`: one state set, several sets with a partly
accepted state, and unknown accepted states.
- Client: `vitest`, 71 tests pass, and `tsc` is clean.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant